FDL - Nuprl Lemma : es-pplus_functionality_wrt_rev

Nuprl Lemma : es-pplus_functionality_wrt_rev_implies

es:ES, e1:E, e2:{e:E| loc(e) = loc(e1)

Id }, p,

p':({e:E| loc(e) = loc(e1)

Id }

{e:E| loc(e) = loc(e1)

Id }

Prop).
(

a, b:{e:E| loc(e) = loc(e1)

Id }. (a

[e1, e2])

{p(a,b)

p'(a,b)})

{[e1,e2]~([a,b].p(a,b))+

[e1,e2]~([a,b].p'(a,b))+}

Definitions {T}, t T, P Q, x:A. B(x), [e1,e2]~([a,b].p(a;b))+, ES, E, loc(e), Id, Prop, x(s1,s2), P Q, [e, e'], (x l)

Lemmas es-pstar-q functionality wrt rev implies, l member wf, es-interval wf, guard wf, rev implies wf, Id wf, es-loc wf, es-E wf, event system wf

Definitions	{T}, t T, P Q, x:A. B(x), [e1,e2]~([a,b].p(a;b))+, ES, E, loc(e), Id, Prop, x(s1,s2), P Q, [e, e'], (x l)
Lemmas	es-pstar-q functionality wrt rev implies, l member wf, es-interval wf, guard wf, rev implies wf, Id wf, es-loc wf, es-E wf, event system wf